(module checker (lib "eopl.ss" "eopl")
  (require "drscheme-init.scm")
  (require "lang.scm")
  (provide type-to-external-form type-of-expression type-of-program)

  (define check-equal-type!
    (lambda (t1 t2 exp)
      (if (equal? t1 t2) 
        #t
        (eopl:error 'check-equal-type!  
          "Types didn't match: ~s != ~a in~%~a"
          (type-to-external-form t1)
          (type-to-external-form t2)
          exp))))
  
  (define type-to-external-form
    (lambda (ty)
      (cases type ty
        (int-type () 'int)
        (bool-type () 'bool)
        (list-type (ty) (list 'listof (type-to-external-form ty)))
        (proc-type (arg-types result-type)
          (list
            ;;(type-to-external-form arg-types)
           (letrec
               ((type-2-ext 
                 (lambda (args)
                   (if (null? args)
                       ()
                       (list (type-to-external-form
                              (car args)) '*
                             (type-2-ext (cdr args)))))))
             (type-2-ext arg-types))
            '->
            (type-to-external-form result-type))))))
  
  ;;;;;;;;;;;;;;;; The Type Checker ;;;;;;;;;;;;;;;;
  
  (define type-of-program
    (lambda (pgm)
      (cases program pgm
        (a-program (exp1) 
          (type-of-expression exp1 (init-tenv))))))
  
  (define type-of-expression
    (lambda (exp tenv)
      (cases expression exp
        (const-exp (num) (int-type))
        
        (diff-exp (exp1 exp2)
          (let ((type1 (type-of-expression exp1 tenv))
                (type2 (type-of-expression exp2 tenv)))
            (check-equal-type! type1 (int-type) exp1)
            (check-equal-type! type2 (int-type) exp2)
            (int-type)))
        
        (zero?-exp (exp1)
          (let ((type1 (type-of-expression exp1 tenv)))
            (check-equal-type! type1 (int-type) exp1)
            (bool-type)))
        
        (if-exp (exp1 exp2 exp3)
          (let ((ty1 (type-of-expression exp1 tenv))
                (ty2 (type-of-expression exp2 tenv))
                (ty3 (type-of-expression exp3 tenv)))
            (check-equal-type! ty1 (bool-type) exp1)
            (check-equal-type! ty2 ty3 exp)
            ty2))
        
        (var-exp (var) (apply-tenv tenv var))
;;(type-of  exp1  tenv) = t1
;;(type-of  exp2  tenv) = t2
;;   ….
;;(type-of  expn  tenv) = tn
;;(type-of  body  [var1=t1,var2=t2…varn=tn]tenv) = t
;;--------------------------------------------------        
;;(type-of   ( let-exp  vars  exps  body)   tenv) = t
         
        (let-exp (vars exps body)
          (let (
                (rhs-types 
                 ;;(type-of-expression exp1 tenv)
                 (letrec
                     ((get-rhs-types
                       (lambda (expressions tenv)
                         (if (null? expressions)
                             ()
                             (cons
                              (type-of-expression 
                               (car expressions) tenv)
                              (get-rhs-types 
                               (cdr expressions)
                               tenv))))))
                   (get-rhs-types exps tenv))
                 )
                )
            (type-of-expression body 
                                ;;(extend-tenv var rhs-type tenv)
                                (letrec
                                    ((extend-tenv-let
                                      (lambda (variables types env)
                                        (if (null? variables)
                                            env
                                            (let
                                                ((new-env (extend-tenv 
                                                           (car variables) 
                                                           (car types) env)))
                                              (extend-tenv-let
                                               (cdr variables)
                                               (cdr types)
                                               new-env)
                                              )
                                            )
                                        )
                                      )
                                     )
                                  (extend-tenv-let vars rhs-types tenv))
                                )
            ))
                                
;;(type-of  body  [bvar1=t1, bvar2=t2, bvar3=t3…bvarn=tn])  =  t
;;--------------------------------------------------------------------------        
;;(type-of  (proc-exp  bvar-types  bvars  body)  tenv)      =  (t1*t2*…tn->t)        
        (proc-exp (bvars bvar-types  body)
          (let ((result-type
                  (type-of-expression body
                    (letrec
                        ((extend-tenv-proc
                          (lambda (vars var-types env)
                            (if (null? vars) env
                            (let ((new-tenv (extend-tenv (car vars)
                                                         (car var-types)
                                                         env)))
                              (extend-tenv-proc (cdr vars)
                                               (cdr var-types)
                                               new-tenv))))))
                        (extend-tenv-proc bvars bvar-types tenv)))))
            (proc-type bvar-types result-type)))
        
        (call-exp (rator rands) 
          (let ((rator-type (type-of-expression rator tenv))
                ;;(rand-type  (type-of-expression rand tenv))
                (rand-types 
                 (letrec
                    ((get-rand-types
                      (lambda (operands env)
                        (if (null? operands) 
                            ()
                            (cons (type-of-expression (car operands) tenv)
                                  (get-rand-types 
                                   (cdr operands)
                                   tenv))))))
                  (get-rand-types rands tenv))))
            (cases type rator-type
              (proc-type (arg-types result-type)
                (begin
                  (check-equal-type! arg-types rand-types rands)
                  result-type))
              (else
                (eopl:error 'type-of-expression
                  "Rator not a proc type:~%~s~%had rator type ~s"   
                  rator (type-to-external-form rator-type))))))

        (list-exp (e es)
                  (letrec 
                      ((type-of-list-exps
                        (lambda (e es)
                          (let ((ty1 (type-of-expression e tenv)))
                            (if (null? es)
                                (list-type ty1)
                                (let ((ty2 (type-of-expression (car es) tenv)))
                                  (if (equal? ty1 ty2)
                                      (type-of-list-exps (car es) (cdr es))
                                      (eopl:error 'type-of-list-exp  
                                                  "Types didn't match: ~s != ~a"
                                                  (type-to-external-form ty1)
                                                  (type-to-external-form ty2)
                                                  ))))))))
                    (type-of-list-exps e es)))

        (cons-exp (e1 e2)
                  
                  (let ((ty1 (type-of-expression e1 tenv))
                        (ty2 (type-of-expression e2 tenv)))
                    
                    (list-type ty1)
                    ))        
        (null-exp (exp)
                  (let ((ty1 (type-of-expression exp tenv)))
                    (bool-type)))
        
        (emptylist-exp (type)
                       (list-type type))
        
;;(car  type-of  (list-exp e1 (e2… en))  tenv)               =t
;;--------------------------------------------------------------        
;;(type-of  car  (list-exp e1 (e2… en))  tenv)               = t        
        (car-exp (expressions)
                  (type-of-expression (car expressions) tenv))
        
        
;;(cdr  type-of  (list-exp e1 (e2… en))  tenv)               =t
;;---------------------------------------------------------------        
;;(type-of  cdr  (list-exp e1 (e2… en))  tenv)               = t
        (cdr-exp (expressions) 
                 (type-of-expression (list-exp (car expressions)
                                                             (cdr expressions)) tenv))
        
        (letrec-exp (proc-result-type 
                      proc-name 
                      bvars 
                      bvar-types 
                      proc-body
                      letrec-body)
          (let ((tenv-for-letrec-body
                  (extend-tenv 
                    proc-name
                    (proc-type bvar-types proc-result-type)
                    tenv)))
            (let ((proc-body-type
                    (type-of-expression 
                     proc-body
                     (letrec
                         ((extend-env-letrec
                           (lambda (vars 
                                    var-types
                                    env)
                             (if (null? vars)
                                 env
                                 (let
                                     ((new-env 
                                       (extend-tenv
                                        (car vars)
                                        (car var-types)
                                        env)))
                                   (extend-env-letrec
                                    (cdr vars)
                                    (cdr var-types)
                                    new-env))))))
                       (extend-env-letrec
                        bvars
                        bvar-types
                        tenv-for-letrec-body))
                                   
                                        
;                      (extend-tenv
;                        bvar
;                        bvar-type
;                        tenv-for-letrec-body)
                      ))) ;; !!
              (check-equal-type!
                proc-body-type proc-result-type proc-body)
              (type-of-expression letrec-body tenv-for-letrec-body))))
        
        )))
    
    ;;;;;;;;;;;;;;;; type environments ;;;;;;;;;;;;;;;;
    
  (define-datatype type-environment type-environment?
    (empty-tenv-record)
    (extended-tenv-record
      (sym symbol?)
      (type type?)
      (tenv type-environment?)))
    
  (define empty-tenv empty-tenv-record)
  (define extend-tenv extended-tenv-record)
    
  (define apply-tenv 
    (lambda (tenv sym)
      (cases type-environment tenv
        (empty-tenv-record ()
          (eopl:error 'apply-tenv "Unbound variable ~s" sym))
        (extended-tenv-record (sym1 val1 old-env)
          (if (eqv? sym sym1) 
            val1
            (apply-tenv old-env sym))))))
  
  (define init-tenv
    (lambda ()
      (extend-tenv 'x (int-type) 
        (extend-tenv 'v (int-type)
          (extend-tenv 'i (int-type)
            (empty-tenv))))))
  )